Nuprl Lemma : t_iterate_wf
4,23
postcript
pdf
E
,
A
:Type,
l
:(
E
A
),
n
:(
A
A
A
),
t
:Tree(
E
). t_iterate(
l
;
n
;
t
)
A
latex
Definitions
Tree(
E
)
,
x
:
A
.
B
(
x
)
,
tree_con(
E
;
T
)
,
Case tree_leaf(
x
) =>
body
(
x
)
cont
,
Case(
value
)
body
,
Case
x
;
y
=>
body
(
x
;
y
)
cont
,
{
T
}
,
t_iterate(
l
;
n
;
t
)
,
t
T
Lemmas
tree
wf
origin
E, A:Type, l:(E
A), n:(AAA), t:Tree(E). t_iterate(l;n;t) 
A E, A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t) A x:A. B(x) T